1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
/*!
Evaluation contexts
*/
use super::*;

mod normal_form;
mod reduce_until;
pub use normal_form::*;
pub use reduce_until::*;

/// Add reduction to an evaluation context
#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Default)]
pub struct Reduce<E, C> {
    /// The underlying evaluation context
    pub eval_ctx: E,
    /// This reduction's configuration
    pub cfg: C,
}

impl<E, C> Reduce<E, C>
where
    E: EvalCtx,
    C: ReductionConfig,
{
    /// Nullify this reduction context
    pub fn nullify(&mut self) -> Reduce<SubstVec<&mut E::Ctx>, &mut C::AsRef> {
        let nullified = Reduce {
            eval_ctx: SubstVec::new(self.eval_ctx.ctx()),
            cfg: self.cfg.as_ref_mut(),
        };
        debug_assert!(nullified.is_var_null());
        nullified
    }
}

/// A reduction configuration
pub trait ReductionConfig {
    /// Get this reduction configuration as a reference
    type AsRef: ReductionConfig;

    /// Register a pushed substitution.
    fn register_push_subst(&mut self, subst: &TermId) -> Result<(), Error>;

    /// Register a popped substitution.
    fn register_pop_subst(&mut self) -> Result<(), Error>;

    /// Register a beta reduction: return whether to terminate beta reduction (`Error::StopReduction`)
    fn register_beta(&mut self) -> Result<(), Error>;

    /// Register an eta reduction: return whether to terminate eta reduction (`Error::StopReduction`)
    fn register_eta(&mut self) -> Result<(), Error>;

    /// Given a term, whether to attempt an eta reduction or terminate (`Error::StopReduction`)
    fn eta(&self, term: &Term, ctx: &mut (impl TyCtxMut + ?Sized)) -> Result<bool, Error>;

    /// Given a term, whether to attempt a subterm reduction or terminate (`Error::StopReduction`)
    fn sub(&self, term: &Term, ctx: &mut (impl TyCtxMut + ?Sized)) -> Result<bool, Error>;

    /// Given a term, whether to attempt a head reduction or terminate (`Error::StopReduction`)
    fn head(&self, term: &Term, ctx: &mut (impl TyCtxMut + ?Sized)) -> Result<bool, Error>;

    /// Get whether a term with the given filter intersects with this context
    fn intersects(&self, filter: VarFilter, code: Code, form: Form) -> bool;

    /// Get this reduction configuration as a mutable reference
    fn as_ref_mut(&mut self) -> &mut Self::AsRef;
}

impl<C> ReductionConfig for &'_ mut C
where
    C: ReductionConfig,
{
    type AsRef = C::AsRef;

    #[inline]
    fn register_push_subst(&mut self, subst: &TermId) -> Result<(), Error> {
        (**self).register_push_subst(subst)
    }

    #[inline]
    fn register_pop_subst(&mut self) -> Result<(), Error> {
        (**self).register_pop_subst()
    }

    #[inline]
    fn register_beta(&mut self) -> Result<(), Error> {
        (**self).register_beta()
    }

    #[inline]
    fn register_eta(&mut self) -> Result<(), Error> {
        (**self).register_eta()
    }

    #[inline]
    fn eta(&self, term: &Term, ctx: &mut (impl TyCtxMut + ?Sized)) -> Result<bool, Error> {
        (**self).eta(term, ctx)
    }

    #[inline]
    fn sub(&self, term: &Term, ctx: &mut (impl TyCtxMut + ?Sized)) -> Result<bool, Error> {
        (**self).sub(term, ctx)
    }

    #[inline]
    fn head(&self, term: &Term, ctx: &mut (impl TyCtxMut + ?Sized)) -> Result<bool, Error> {
        (**self).head(term, ctx)
    }

    #[inline]
    fn intersects(&self, filter: VarFilter, code: Code, form: Form) -> bool {
        (**self).intersects(filter, code, form)
    }

    #[inline]
    fn as_ref_mut(&mut self) -> &mut Self::AsRef {
        (**self).as_ref_mut()
    }
}

impl<E: EvalCtx, C: ReductionConfig> SubstCtx for Reduce<E, C> {
    type Ctx = E::Ctx;

    fn try_subst(&mut self, start_term: &Term) -> Option<Result<Option<TermId>, Error>> {
        // Begin substitution attempt
        let mut curr = None;
        loop {
            // Whether anything changed this iteration
            let mut changed = false;

            // Should we perform a head reduction?
            match self
                .cfg
                .head(curr.as_deref().unwrap_or(start_term), self.eval_ctx.ctx())
            {
                // Maybe...
                Ok(head) => {
                    let subst = if head {
                        // Yes, perform the head reduction
                        let mut args = smallvec![];
                        let applied = curr
                            .as_deref()
                            .unwrap_or(start_term)
                            .apply(&mut args, &mut self.eval_ctx);

                        // Check invariants
                        debug_assert_eq!(args.len(), 0);

                        applied
                    } else {
                        // No, just recursively substitute in the evaluation context
                        start_term.subst_id(&mut self.eval_ctx)
                    };

                    // Handle the result
                    match subst {
                        // Successful, modifying reduction
                        Ok(Some(term)) => {
                            // Handle this
                            match self.cfg.register_beta() {
                                // Keep going
                                Ok(()) => {}
                                // Terminate
                                Err(Error::StopReduction) => return Some(Ok(Some(term))),
                                // Fail
                                Err(err) => return Some(Err(err)),
                            }
                            // Change the current value
                            curr = Some(term);
                            // Set that a beta reduction has been performed
                            changed = true;
                        }
                        // Successful null reduction
                        Ok(None) => {}
                        // Terminate
                        Err(Error::StopReduction) => return Some(Ok(curr)),
                        // Fail
                        Err(err) => return Some(Err(err)),
                    }
                }
                // Terminate
                Err(Error::StopReduction) => return Some(Ok(curr)),
                // Fail
                Err(err) => return Some(Err(err)),
            };

            // Now, perform eta reductions until we can't anymore
            loop {
                // Get a pointer to the term for this iteration
                let curr_term = curr.as_deref().unwrap_or(start_term);

                // Should we perform an eta reduction?
                match self.cfg.eta(curr_term, self.eval_ctx.ctx()) {
                    // Yes, attempt an eta reduction
                    Ok(true) => {
                        // Is this term a lambda function?
                        if let Term::Lambda(term) = curr_term {
                            // Yes. Does this term eta reduce?
                            if let Some(term) = term.eta(self.ctx()) {
                                // Yes. Handle this
                                match self.cfg.register_eta() {
                                    // Keep going
                                    Ok(()) => {}
                                    // Terminate
                                    Err(Error::StopReduction) => return Some(Ok(Some(term))),
                                    // Fail
                                    Err(err) => return Some(Err(err)),
                                }
                                // Change the current value
                                curr = Some(term);
                                // Set that an eta reduction was performed this iteration
                                changed = true;
                            } else {
                                // This term does not eta-reduce, so break.
                                break;
                            }
                        } else {
                            // We can't eta-reduce a non-lambda, so break.
                            break;
                        }
                    }
                    // No, don't attempt an eta reduction: break the loop here
                    Ok(false) => break,
                    // Terminate
                    Err(Error::StopReduction) => return Some(Ok(curr)),
                    // Fail
                    Err(err) => return Some(Err(err)),
                };
            }

            // Do we have a changed value?
            if let Some(curr_term) = &curr {
                // Yes: was there a change this iteration?
                if changed {
                    // Yes, so is this context null?
                    if self.is_var_null() {
                        // Yes, so "recursively" call this function via continue. tail-recursion ftw.
                        continue;
                    } else {
                        // No, so finish the substitution in the nullified version of this context
                        return match curr_term.subst_rec(&mut self.nullify()) {
                            // Substitute
                            Ok(Some(term)) => Some(Ok(Some(term))),
                            // No change
                            Ok(None) => Some(Ok(Some(curr_term.clone()))),
                            // Fail
                            Err(err) => Some(Err(err)),
                        };
                    }
                }
                // No, so do we perform recursive substitutions?
                else {
                    match self.cfg.sub(curr_term, self.eval_ctx.ctx()) {
                        Ok(true) => {
                            // Yes, so is this context null?
                            let subst = if self.is_var_null() {
                                // Yes, so perform a recursive fallback substitution in this context
                                curr_term.subst_rec_id(self)
                            } else {
                                // No, so perform a recursive fallback substitution in the nullified version of this context
                                curr_term.subst_rec_id(&mut self.nullify())
                            };
                            // Handle the result:
                            return match subst {
                                Ok(result) => Some(Ok(result.or(curr))),
                                Err(err) => Some(Err(err)),
                            };
                        }
                        // No: then just return the changed value as final
                        Ok(false) | Err(Error::StopReduction) => {
                            return Some(Ok(curr));
                        }
                        Err(err) => return Some(Err(err)),
                    }
                }
            } else {
                // No. Begin with sanity checks:

                // If there's no current value, there can't have been a change ever, and hence not now!
                debug_assert!(!changed);

                // Do we perform recursive substitutions?
                match self.cfg.sub(start_term, self.eval_ctx.ctx()) {
                    Ok(true) => {
                        // Yes, so is this context null?
                        if self.is_var_null() {
                            // Yes, so fallthrough in this context
                            return None;
                        } else {
                            // No, so perform a recursive fallback substitution in the nullified version of this context
                            return Some(start_term.subst_rec_id(&mut self.nullify()));
                        }
                    }
                    Ok(false) | Err(Error::StopReduction) => {
                        // No, so just return the current term
                        return Some(Ok(curr));
                    }
                    Err(err) => return Some(Err(err)),
                }
            }
        }
    }

    fn subst_constrain(
        &mut self,
        ix: u32,
        annot: Option<&TermId>,
    ) -> Result<Option<TermId>, Error> {
        //TODO: try to avoid repeating substitutions?
        let result = self.eval_ctx.subst_constrain(ix, annot)?;
        if let Some(result) = result {
            result.subst_rec(&mut self.nullify())
        } else {
            Ok(None)
        }
    }

    fn subst_var(&mut self, ix: u32, annot: Option<&TermId>) -> Result<Option<TermId>, Error> {
        //TODO: try to avoid repeating substitutions?
        let result = self.eval_ctx.subst_var(ix, annot)?;
        if let Some(result) = result {
            result.subst_rec(&mut self.nullify())
        } else {
            Ok(None)
        }
    }

    fn push_param(&mut self, param_ty: Option<&TermId>) -> Result<Option<TermId>, Error> {
        //TODO: normalize types? Why is that so complicated...
        self.eval_ctx.push_param(param_ty)
    }

    fn intersects(&self, filter: VarFilter, code: Code, form: Form) -> bool {
        self.cfg.intersects(filter, code, form) || self.eval_ctx.intersects(filter, code, form)
    }

    #[inline]
    fn ctx(&mut self) -> &mut Self::Ctx {
        self.eval_ctx.ctx()
    }

    #[inline]
    fn cons_ctx(&mut self) -> &mut <Self::Ctx as TyCtxMut>::ConsCtx {
        self.eval_ctx.cons_ctx()
    }

    #[inline]
    fn eq_ctx(&mut self) -> &mut <Self::Ctx as TyCtxMut>::TermEqCtx {
        self.eval_ctx.eq_ctx()
    }

    #[inline]
    fn push_param_ctx(&mut self, param_ty: Option<&TermId>) -> Result<(), Error> {
        self.eval_ctx.push_param_ctx(param_ty)
    }

    #[inline]
    fn pop_param(&mut self) -> Result<(), Error> {
        self.eval_ctx.pop_param()
    }

    #[inline]
    fn is_var_null(&self) -> bool {
        self.eval_ctx.is_var_null()
    }
}

impl<E: EvalCtx, C: ReductionConfig> EvalCtx for Reduce<E, C> {
    fn push_subst(&mut self, subst: TermId) -> Result<(), Error> {
        self.cfg.register_push_subst(&subst)?;
        self.eval_ctx.push_subst(subst)
    }

    fn pop_subst(&mut self) -> Result<(), Error> {
        self.cfg.register_pop_subst()?;
        self.eval_ctx.pop_subst()
    }
}